1. Field of the Invention
The present invention relates to digital circuitry designs, and more specifically systems and methods of reducing an original circuit design into a simplified circuit design.
2. Description of Related Art
Digital circuitry with memory elements may be modeled using state equations and state variables to describe the behavior and state of the system. The synthesis and verification of state variable models often requires a great deal of computational resources. Simplifying the model to reduce the number of state variables, or simplifying the logic that defines state transitions, lessens the computational cost of analyzing the model, for example, to verify that it conforms to a given specification. The ability to reduce design size may make the difference in whether or not it is feasible to use a verification algorithm to expose a design flaw.
Formal and semi-formal verification techniques are powerful tools for the construction of correct logic designs. They have the power to expose even the most probabilistically uncommon scenario that may result in a functional design failure, and ultimately have the power to prove that the design is correct by showing that no failing scenario exists. Unfortunately, formal verification techniques require computational resources which are exponential with respect to the size of the design under test. Semi-formal verification techniques allow formal algorithms to be applied to larger designs through resource-bounding, though at the expense of incomplete verification coverage.
One conventional approach to improve the merging of gate was described in a paper by Qi Zhu et al. entitled “SAT Sweeping with Local Observability Don't-Cares,” published for the 2006 Design Automation Conference (pps. 229-234). This paper discusses the use of “observability don't cares” (ODCs) to enhance merging. ODC-enhanced merging generalizes upon traditional merging by enabling the merging of two gates which are demonstrated at any point in time to either be equivalent, or to differ without altering the design behavior with respect to some fanout boundary.
What is needed is an improved way of reducing a complex digital circuitry design to a more manageable size for synthesis and verification.